T:Type, L:T List, R:(||L||||L||Prop), P:(||L||Prop).
Refl(||L||;_1,_2.R(_1,_2))  causal_order(L;R;P;P) 

latex

Definitions	t  T, {i..j}, x:A. B(x), AB, Prop, P & Q, ij, ||as||, x:A. B(x), x,y. t(x;y), Refl(T;x,y.E(x;y)), P  Q, False, A, i  j < k, causal_order(L;R;P;Q)
Lemmas	refl wf, int seg wf, length wf1, le wf